Left Termination proof of /tmp/tmpGZ3lPn/shuffle.pl

Left Termination of the query pattern query(b) w.r.t. the given Prolog program could successfully be proven:

↳ PROLOG

  ↳ PrologToPiTRSProof

append₃(nil₀, XS, XS).
append₃(cons₂(X, XS), YS, cons₂(X, ZS)) :- append₃(XS, YS, ZS).
reverse₂(nil₀, nil₀).
reverse₂(cons₂(X, nil₀), cons₂(X, nil₀)).
reverse₂(cons₂(X, XS), YS) :- reverse₂(XS, ZS), append₃(ZS, cons₂(X, nil₀), YS).
shuffle₂(nil₀, nil₀).
shuffle₂(cons₂(X, XS), cons₂(X, YS)) :- reverse₂(XS, ZS), shuffle₂(ZS, YS).
query₁(XS) :- shuffle₂(cons₂(X, XS), YS).

With regard to the inferred argument filtering the predicates were used in the following modes:
query₁: (b)
shuffle₂: (b,f)
reverse₂: (b,f)
append₃: (b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

query_1_in_g₁(XS) -> if_query_1_in_1_g₂(XS, shuffle_2_in_ga₂(cons_2₂(X, XS), YS))
shuffle_2_in_ga₂(nil_0, nil_0) -> shuffle_2_out_ga₂(nil_0, nil_0)
shuffle_2_in_ga₂(cons_2₂(X, XS), cons_2₂(X, YS)) -> if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
reverse_2_in_ga₂(nil_0, nil_0) -> reverse_2_out_ga₂(nil_0, nil_0)
reverse_2_in_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0)) -> reverse_2_out_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0))
reverse_2_in_ga₂(cons_2₂(X, XS), YS) -> if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_in_gga₃(ZS, cons_2₂(X, nil_0), YS))
append_3_in_gga₃(nil_0, XS, XS) -> append_3_out_gga₃(nil_0, XS, XS)
append_3_in_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_in_gga₃(XS, YS, ZS))
if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_out_gga₃(XS, YS, ZS)) -> append_3_out_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS))
if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_out_gga₃(ZS, cons_2₂(X, nil_0), YS)) -> reverse_2_out_ga₂(cons_2₂(X, XS), YS)
if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_in_ga₂(ZS, YS))
if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_out_ga₂(ZS, YS)) -> shuffle_2_out_ga₂(cons_2₂(X, XS), cons_2₂(X, YS))
if_query_1_in_1_g₂(XS, shuffle_2_out_ga₂(cons_2₂(X, XS), YS)) -> query_1_out_g₁(XS)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

query_1_in_g₁(XS) -> if_query_1_in_1_g₂(XS, shuffle_2_in_ga₂(cons_2₂(X, XS), YS))
shuffle_2_in_ga₂(nil_0, nil_0) -> shuffle_2_out_ga₂(nil_0, nil_0)
shuffle_2_in_ga₂(cons_2₂(X, XS), cons_2₂(X, YS)) -> if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
reverse_2_in_ga₂(nil_0, nil_0) -> reverse_2_out_ga₂(nil_0, nil_0)
reverse_2_in_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0)) -> reverse_2_out_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0))
reverse_2_in_ga₂(cons_2₂(X, XS), YS) -> if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_in_gga₃(ZS, cons_2₂(X, nil_0), YS))
append_3_in_gga₃(nil_0, XS, XS) -> append_3_out_gga₃(nil_0, XS, XS)
append_3_in_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_in_gga₃(XS, YS, ZS))
if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_out_gga₃(XS, YS, ZS)) -> append_3_out_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS))
if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_out_gga₃(ZS, cons_2₂(X, nil_0), YS)) -> reverse_2_out_ga₂(cons_2₂(X, XS), YS)
if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_in_ga₂(ZS, YS))
if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_out_ga₂(ZS, YS)) -> shuffle_2_out_ga₂(cons_2₂(X, XS), cons_2₂(X, YS))
if_query_1_in_1_g₂(XS, shuffle_2_out_ga₂(cons_2₂(X, XS), YS)) -> query_1_out_g₁(XS)

QUERY_1_IN_G₁(XS) -> IF_QUERY_1_IN_1_G₂(XS, shuffle_2_in_ga₂(cons_2₂(X, XS), YS))
QUERY_1_IN_G₁(XS) -> SHUFFLE_2_IN_GA₂(cons_2₂(X, XS), YS)
SHUFFLE_2_IN_GA₂(cons_2₂(X, XS), cons_2₂(X, YS)) -> IF_SHUFFLE_2_IN_1_GA₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
SHUFFLE_2_IN_GA₂(cons_2₂(X, XS), cons_2₂(X, YS)) -> REVERSE_2_IN_GA₂(XS, ZS)
REVERSE_2_IN_GA₂(cons_2₂(X, XS), YS) -> IF_REVERSE_2_IN_1_GA₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
REVERSE_2_IN_GA₂(cons_2₂(X, XS), YS) -> REVERSE_2_IN_GA₂(XS, ZS)
IF_REVERSE_2_IN_1_GA₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> IF_REVERSE_2_IN_2_GA₅(X, XS, YS, ZS, append_3_in_gga₃(ZS, cons_2₂(X, nil_0), YS))
IF_REVERSE_2_IN_1_GA₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> APPEND_3_IN_GGA₃(ZS, cons_2₂(X, nil_0), YS)
APPEND_3_IN_GGA₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> IF_APPEND_3_IN_1_GGA₅(X, XS, YS, ZS, append_3_in_gga₃(XS, YS, ZS))
APPEND_3_IN_GGA₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> APPEND_3_IN_GGA₃(XS, YS, ZS)
IF_SHUFFLE_2_IN_1_GA₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> IF_SHUFFLE_2_IN_2_GA₅(X, XS, YS, ZS, shuffle_2_in_ga₂(ZS, YS))
IF_SHUFFLE_2_IN_1_GA₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> SHUFFLE_2_IN_GA₂(ZS, YS)

The TRS R consists of the following rules:

query_1_in_g₁(XS) -> if_query_1_in_1_g₂(XS, shuffle_2_in_ga₂(cons_2₂(X, XS), YS))
shuffle_2_in_ga₂(nil_0, nil_0) -> shuffle_2_out_ga₂(nil_0, nil_0)
shuffle_2_in_ga₂(cons_2₂(X, XS), cons_2₂(X, YS)) -> if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
reverse_2_in_ga₂(nil_0, nil_0) -> reverse_2_out_ga₂(nil_0, nil_0)
reverse_2_in_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0)) -> reverse_2_out_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0))
reverse_2_in_ga₂(cons_2₂(X, XS), YS) -> if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_in_gga₃(ZS, cons_2₂(X, nil_0), YS))
append_3_in_gga₃(nil_0, XS, XS) -> append_3_out_gga₃(nil_0, XS, XS)
append_3_in_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_in_gga₃(XS, YS, ZS))
if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_out_gga₃(XS, YS, ZS)) -> append_3_out_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS))
if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_out_gga₃(ZS, cons_2₂(X, nil_0), YS)) -> reverse_2_out_ga₂(cons_2₂(X, XS), YS)
if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_in_ga₂(ZS, YS))
if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_out_ga₂(ZS, YS)) -> shuffle_2_out_ga₂(cons_2₂(X, XS), cons_2₂(X, YS))
if_query_1_in_1_g₂(XS, shuffle_2_out_ga₂(cons_2₂(X, XS), YS)) -> query_1_out_g₁(XS)

The argument filtering Pi contains the following mapping:
query_1_in_g₁(x1) = query_1_in_g₁(x1)
nil_0 = nil_0
cons_2₂(x1, x2) = cons_2₁(x2)
if_query_1_in_1_g₂(x1, x2) = if_query_1_in_1_g₁(x2)
shuffle_2_in_ga₂(x1, x2) = shuffle_2_in_ga₁(x1)
shuffle_2_out_ga₂(x1, x2) = shuffle_2_out_ga₁(x2)
if_shuffle_2_in_1_ga₄(x1, x2, x3, x4) = if_shuffle_2_in_1_ga₁(x4)
reverse_2_in_ga₂(x1, x2) = reverse_2_in_ga₁(x1)
reverse_2_out_ga₂(x1, x2) = reverse_2_out_ga₁(x2)
if_reverse_2_in_1_ga₄(x1, x2, x3, x4) = if_reverse_2_in_1_ga₁(x4)
if_reverse_2_in_2_ga₅(x1, x2, x3, x4, x5) = if_reverse_2_in_2_ga₁(x5)
append_3_in_gga₃(x1, x2, x3) = append_3_in_gga₂(x1, x2)
append_3_out_gga₃(x1, x2, x3) = append_3_out_gga₁(x3)
if_append_3_in_1_gga₅(x1, x2, x3, x4, x5) = if_append_3_in_1_gga₁(x5)
if_shuffle_2_in_2_ga₅(x1, x2, x3, x4, x5) = if_shuffle_2_in_2_ga₁(x5)
query_1_out_g₁(x1) = query_1_out_g
IF_SHUFFLE_2_IN_2_GA₅(x1, x2, x3, x4, x5) = IF_SHUFFLE_2_IN_2_GA₁(x5)
IF_QUERY_1_IN_1_G₂(x1, x2) = IF_QUERY_1_IN_1_G₁(x2)
IF_APPEND_3_IN_1_GGA₅(x1, x2, x3, x4, x5) = IF_APPEND_3_IN_1_GGA₁(x5)
SHUFFLE_2_IN_GA₂(x1, x2) = SHUFFLE_2_IN_GA₁(x1)
IF_SHUFFLE_2_IN_1_GA₄(x1, x2, x3, x4) = IF_SHUFFLE_2_IN_1_GA₁(x4)
REVERSE_2_IN_GA₂(x1, x2) = REVERSE_2_IN_GA₁(x1)
IF_REVERSE_2_IN_2_GA₅(x1, x2, x3, x4, x5) = IF_REVERSE_2_IN_2_GA₁(x5)
QUERY_1_IN_G₁(x1) = QUERY_1_IN_G₁(x1)
APPEND_3_IN_GGA₃(x1, x2, x3) = APPEND_3_IN_GGA₂(x1, x2)
IF_REVERSE_2_IN_1_GA₄(x1, x2, x3, x4) = IF_REVERSE_2_IN_1_GA₁(x4)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

QUERY_1_IN_G₁(XS) -> IF_QUERY_1_IN_1_G₂(XS, shuffle_2_in_ga₂(cons_2₂(X, XS), YS))
QUERY_1_IN_G₁(XS) -> SHUFFLE_2_IN_GA₂(cons_2₂(X, XS), YS)
SHUFFLE_2_IN_GA₂(cons_2₂(X, XS), cons_2₂(X, YS)) -> IF_SHUFFLE_2_IN_1_GA₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
SHUFFLE_2_IN_GA₂(cons_2₂(X, XS), cons_2₂(X, YS)) -> REVERSE_2_IN_GA₂(XS, ZS)
REVERSE_2_IN_GA₂(cons_2₂(X, XS), YS) -> IF_REVERSE_2_IN_1_GA₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
REVERSE_2_IN_GA₂(cons_2₂(X, XS), YS) -> REVERSE_2_IN_GA₂(XS, ZS)
IF_REVERSE_2_IN_1_GA₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> IF_REVERSE_2_IN_2_GA₅(X, XS, YS, ZS, append_3_in_gga₃(ZS, cons_2₂(X, nil_0), YS))
IF_REVERSE_2_IN_1_GA₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> APPEND_3_IN_GGA₃(ZS, cons_2₂(X, nil_0), YS)
APPEND_3_IN_GGA₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> IF_APPEND_3_IN_1_GGA₅(X, XS, YS, ZS, append_3_in_gga₃(XS, YS, ZS))
APPEND_3_IN_GGA₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> APPEND_3_IN_GGA₃(XS, YS, ZS)
IF_SHUFFLE_2_IN_1_GA₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> IF_SHUFFLE_2_IN_2_GA₅(X, XS, YS, ZS, shuffle_2_in_ga₂(ZS, YS))
IF_SHUFFLE_2_IN_1_GA₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> SHUFFLE_2_IN_GA₂(ZS, YS)

The TRS R consists of the following rules:

query_1_in_g₁(XS) -> if_query_1_in_1_g₂(XS, shuffle_2_in_ga₂(cons_2₂(X, XS), YS))
shuffle_2_in_ga₂(nil_0, nil_0) -> shuffle_2_out_ga₂(nil_0, nil_0)
shuffle_2_in_ga₂(cons_2₂(X, XS), cons_2₂(X, YS)) -> if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
reverse_2_in_ga₂(nil_0, nil_0) -> reverse_2_out_ga₂(nil_0, nil_0)
reverse_2_in_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0)) -> reverse_2_out_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0))
reverse_2_in_ga₂(cons_2₂(X, XS), YS) -> if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_in_gga₃(ZS, cons_2₂(X, nil_0), YS))
append_3_in_gga₃(nil_0, XS, XS) -> append_3_out_gga₃(nil_0, XS, XS)
append_3_in_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_in_gga₃(XS, YS, ZS))
if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_out_gga₃(XS, YS, ZS)) -> append_3_out_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS))
if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_out_gga₃(ZS, cons_2₂(X, nil_0), YS)) -> reverse_2_out_ga₂(cons_2₂(X, XS), YS)
if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_in_ga₂(ZS, YS))
if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_out_ga₂(ZS, YS)) -> shuffle_2_out_ga₂(cons_2₂(X, XS), cons_2₂(X, YS))
if_query_1_in_1_g₂(XS, shuffle_2_out_ga₂(cons_2₂(X, XS), YS)) -> query_1_out_g₁(XS)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

APPEND_3_IN_GGA₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> APPEND_3_IN_GGA₃(XS, YS, ZS)

The TRS R consists of the following rules:

query_1_in_g₁(XS) -> if_query_1_in_1_g₂(XS, shuffle_2_in_ga₂(cons_2₂(X, XS), YS))
shuffle_2_in_ga₂(nil_0, nil_0) -> shuffle_2_out_ga₂(nil_0, nil_0)
shuffle_2_in_ga₂(cons_2₂(X, XS), cons_2₂(X, YS)) -> if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
reverse_2_in_ga₂(nil_0, nil_0) -> reverse_2_out_ga₂(nil_0, nil_0)
reverse_2_in_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0)) -> reverse_2_out_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0))
reverse_2_in_ga₂(cons_2₂(X, XS), YS) -> if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_in_gga₃(ZS, cons_2₂(X, nil_0), YS))
append_3_in_gga₃(nil_0, XS, XS) -> append_3_out_gga₃(nil_0, XS, XS)
append_3_in_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_in_gga₃(XS, YS, ZS))
if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_out_gga₃(XS, YS, ZS)) -> append_3_out_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS))
if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_out_gga₃(ZS, cons_2₂(X, nil_0), YS)) -> reverse_2_out_ga₂(cons_2₂(X, XS), YS)
if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_in_ga₂(ZS, YS))
if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_out_ga₂(ZS, YS)) -> shuffle_2_out_ga₂(cons_2₂(X, XS), cons_2₂(X, YS))
if_query_1_in_1_g₂(XS, shuffle_2_out_ga₂(cons_2₂(X, XS), YS)) -> query_1_out_g₁(XS)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

APPEND_3_IN_GGA₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> APPEND_3_IN_GGA₃(XS, YS, ZS)

R is empty.
The argument filtering Pi contains the following mapping:
cons_2₂(x1, x2) = cons_2₁(x2)
APPEND_3_IN_GGA₃(x1, x2, x3) = APPEND_3_IN_GGA₂(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

APPEND_3_IN_GGA₂(cons_2₁(XS), YS) -> APPEND_3_IN_GGA₂(XS, YS)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {APPEND_3_IN_GGA₂}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

APPEND_3_IN_GGA₂(cons_2₁(XS), YS) -> APPEND_3_IN_GGA₂(XS, YS)
The graph contains the following edges 1 > 1, 2 >= 2

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

REVERSE_2_IN_GA₂(cons_2₂(X, XS), YS) -> REVERSE_2_IN_GA₂(XS, ZS)

The TRS R consists of the following rules:

query_1_in_g₁(XS) -> if_query_1_in_1_g₂(XS, shuffle_2_in_ga₂(cons_2₂(X, XS), YS))
shuffle_2_in_ga₂(nil_0, nil_0) -> shuffle_2_out_ga₂(nil_0, nil_0)
shuffle_2_in_ga₂(cons_2₂(X, XS), cons_2₂(X, YS)) -> if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
reverse_2_in_ga₂(nil_0, nil_0) -> reverse_2_out_ga₂(nil_0, nil_0)
reverse_2_in_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0)) -> reverse_2_out_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0))
reverse_2_in_ga₂(cons_2₂(X, XS), YS) -> if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_in_gga₃(ZS, cons_2₂(X, nil_0), YS))
append_3_in_gga₃(nil_0, XS, XS) -> append_3_out_gga₃(nil_0, XS, XS)
append_3_in_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_in_gga₃(XS, YS, ZS))
if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_out_gga₃(XS, YS, ZS)) -> append_3_out_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS))
if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_out_gga₃(ZS, cons_2₂(X, nil_0), YS)) -> reverse_2_out_ga₂(cons_2₂(X, XS), YS)
if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_in_ga₂(ZS, YS))
if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_out_ga₂(ZS, YS)) -> shuffle_2_out_ga₂(cons_2₂(X, XS), cons_2₂(X, YS))
if_query_1_in_1_g₂(XS, shuffle_2_out_ga₂(cons_2₂(X, XS), YS)) -> query_1_out_g₁(XS)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

REVERSE_2_IN_GA₂(cons_2₂(X, XS), YS) -> REVERSE_2_IN_GA₂(XS, ZS)

R is empty.
The argument filtering Pi contains the following mapping:
cons_2₂(x1, x2) = cons_2₁(x2)
REVERSE_2_IN_GA₂(x1, x2) = REVERSE_2_IN_GA₁(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

REVERSE_2_IN_GA₁(cons_2₁(XS)) -> REVERSE_2_IN_GA₁(XS)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {REVERSE_2_IN_GA₁}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

REVERSE_2_IN_GA₁(cons_2₁(XS)) -> REVERSE_2_IN_GA₁(XS)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

SHUFFLE_2_IN_GA₂(cons_2₂(X, XS), cons_2₂(X, YS)) -> IF_SHUFFLE_2_IN_1_GA₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
IF_SHUFFLE_2_IN_1_GA₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> SHUFFLE_2_IN_GA₂(ZS, YS)

The TRS R consists of the following rules:

query_1_in_g₁(XS) -> if_query_1_in_1_g₂(XS, shuffle_2_in_ga₂(cons_2₂(X, XS), YS))
shuffle_2_in_ga₂(nil_0, nil_0) -> shuffle_2_out_ga₂(nil_0, nil_0)
shuffle_2_in_ga₂(cons_2₂(X, XS), cons_2₂(X, YS)) -> if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
reverse_2_in_ga₂(nil_0, nil_0) -> reverse_2_out_ga₂(nil_0, nil_0)
reverse_2_in_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0)) -> reverse_2_out_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0))
reverse_2_in_ga₂(cons_2₂(X, XS), YS) -> if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_in_gga₃(ZS, cons_2₂(X, nil_0), YS))
append_3_in_gga₃(nil_0, XS, XS) -> append_3_out_gga₃(nil_0, XS, XS)
append_3_in_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_in_gga₃(XS, YS, ZS))
if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_out_gga₃(XS, YS, ZS)) -> append_3_out_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS))
if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_out_gga₃(ZS, cons_2₂(X, nil_0), YS)) -> reverse_2_out_ga₂(cons_2₂(X, XS), YS)
if_shuffle_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_in_ga₂(ZS, YS))
if_shuffle_2_in_2_ga₅(X, XS, YS, ZS, shuffle_2_out_ga₂(ZS, YS)) -> shuffle_2_out_ga₂(cons_2₂(X, XS), cons_2₂(X, YS))
if_query_1_in_1_g₂(XS, shuffle_2_out_ga₂(cons_2₂(X, XS), YS)) -> query_1_out_g₁(XS)

The argument filtering Pi contains the following mapping:
query_1_in_g₁(x1) = query_1_in_g₁(x1)
nil_0 = nil_0
cons_2₂(x1, x2) = cons_2₁(x2)
if_query_1_in_1_g₂(x1, x2) = if_query_1_in_1_g₁(x2)
shuffle_2_in_ga₂(x1, x2) = shuffle_2_in_ga₁(x1)
shuffle_2_out_ga₂(x1, x2) = shuffle_2_out_ga₁(x2)
if_shuffle_2_in_1_ga₄(x1, x2, x3, x4) = if_shuffle_2_in_1_ga₁(x4)
reverse_2_in_ga₂(x1, x2) = reverse_2_in_ga₁(x1)
reverse_2_out_ga₂(x1, x2) = reverse_2_out_ga₁(x2)
if_reverse_2_in_1_ga₄(x1, x2, x3, x4) = if_reverse_2_in_1_ga₁(x4)
if_reverse_2_in_2_ga₅(x1, x2, x3, x4, x5) = if_reverse_2_in_2_ga₁(x5)
append_3_in_gga₃(x1, x2, x3) = append_3_in_gga₂(x1, x2)
append_3_out_gga₃(x1, x2, x3) = append_3_out_gga₁(x3)
if_append_3_in_1_gga₅(x1, x2, x3, x4, x5) = if_append_3_in_1_gga₁(x5)
if_shuffle_2_in_2_ga₅(x1, x2, x3, x4, x5) = if_shuffle_2_in_2_ga₁(x5)
query_1_out_g₁(x1) = query_1_out_g
SHUFFLE_2_IN_GA₂(x1, x2) = SHUFFLE_2_IN_GA₁(x1)
IF_SHUFFLE_2_IN_1_GA₄(x1, x2, x3, x4) = IF_SHUFFLE_2_IN_1_GA₁(x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

SHUFFLE_2_IN_GA₂(cons_2₂(X, XS), cons_2₂(X, YS)) -> IF_SHUFFLE_2_IN_1_GA₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
IF_SHUFFLE_2_IN_1_GA₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> SHUFFLE_2_IN_GA₂(ZS, YS)

The TRS R consists of the following rules:

reverse_2_in_ga₂(nil_0, nil_0) -> reverse_2_out_ga₂(nil_0, nil_0)
reverse_2_in_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0)) -> reverse_2_out_ga₂(cons_2₂(X, nil_0), cons_2₂(X, nil_0))
reverse_2_in_ga₂(cons_2₂(X, XS), YS) -> if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_in_ga₂(XS, ZS))
if_reverse_2_in_1_ga₄(X, XS, YS, reverse_2_out_ga₂(XS, ZS)) -> if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_in_gga₃(ZS, cons_2₂(X, nil_0), YS))
if_reverse_2_in_2_ga₅(X, XS, YS, ZS, append_3_out_gga₃(ZS, cons_2₂(X, nil_0), YS)) -> reverse_2_out_ga₂(cons_2₂(X, XS), YS)
append_3_in_gga₃(nil_0, XS, XS) -> append_3_out_gga₃(nil_0, XS, XS)
append_3_in_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS)) -> if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_in_gga₃(XS, YS, ZS))
if_append_3_in_1_gga₅(X, XS, YS, ZS, append_3_out_gga₃(XS, YS, ZS)) -> append_3_out_gga₃(cons_2₂(X, XS), YS, cons_2₂(X, ZS))

The argument filtering Pi contains the following mapping:
nil_0 = nil_0
cons_2₂(x1, x2) = cons_2₁(x2)
reverse_2_in_ga₂(x1, x2) = reverse_2_in_ga₁(x1)
reverse_2_out_ga₂(x1, x2) = reverse_2_out_ga₁(x2)
if_reverse_2_in_1_ga₄(x1, x2, x3, x4) = if_reverse_2_in_1_ga₁(x4)
if_reverse_2_in_2_ga₅(x1, x2, x3, x4, x5) = if_reverse_2_in_2_ga₁(x5)
append_3_in_gga₃(x1, x2, x3) = append_3_in_gga₂(x1, x2)
append_3_out_gga₃(x1, x2, x3) = append_3_out_gga₁(x3)
if_append_3_in_1_gga₅(x1, x2, x3, x4, x5) = if_append_3_in_1_gga₁(x5)
SHUFFLE_2_IN_GA₂(x1, x2) = SHUFFLE_2_IN_GA₁(x1)
IF_SHUFFLE_2_IN_1_GA₄(x1, x2, x3, x4) = IF_SHUFFLE_2_IN_1_GA₁(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

SHUFFLE_2_IN_GA₁(cons_2₁(XS)) -> IF_SHUFFLE_2_IN_1_GA₁(reverse_2_in_ga₁(XS))
IF_SHUFFLE_2_IN_1_GA₁(reverse_2_out_ga₁(ZS)) -> SHUFFLE_2_IN_GA₁(ZS)

The TRS R consists of the following rules:

reverse_2_in_ga₁(nil_0) -> reverse_2_out_ga₁(nil_0)
reverse_2_in_ga₁(cons_2₁(nil_0)) -> reverse_2_out_ga₁(cons_2₁(nil_0))
reverse_2_in_ga₁(cons_2₁(XS)) -> if_reverse_2_in_1_ga₁(reverse_2_in_ga₁(XS))
if_reverse_2_in_1_ga₁(reverse_2_out_ga₁(ZS)) -> if_reverse_2_in_2_ga₁(append_3_in_gga₂(ZS, cons_2₁(nil_0)))
if_reverse_2_in_2_ga₁(append_3_out_gga₁(YS)) -> reverse_2_out_ga₁(YS)
append_3_in_gga₂(nil_0, XS) -> append_3_out_gga₁(XS)
append_3_in_gga₂(cons_2₁(XS), YS) -> if_append_3_in_1_gga₁(append_3_in_gga₂(XS, YS))
if_append_3_in_1_gga₁(append_3_out_gga₁(ZS)) -> append_3_out_gga₁(cons_2₁(ZS))

The set Q consists of the following terms:

reverse_2_in_ga₁(x0)
if_reverse_2_in_1_ga₁(x0)
if_reverse_2_in_2_ga₁(x0)
append_3_in_gga₂(x0, x1)
if_append_3_in_1_gga₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_SHUFFLE_2_IN_1_GA₁, SHUFFLE_2_IN_GA₁}.
We used the following order together with the size-change analysis to show that there are no infinite chains for this DP problem.

Order:Polynomial interpretation:

POL(nil_0) = 0
POL(append_3_out_gga₁(x₁)) = x₁
POL(cons_2₁(x₁)) = 1 + x₁
POL(reverse_2_out_ga₁(x₁)) = x₁
POL(if_reverse_2_in_1_ga₁(x₁)) = 1 + x₁
POL(if_append_3_in_1_gga₁(x₁)) = 1 + x₁
POL(reverse_2_in_ga₁(x₁)) = x₁
POL(if_reverse_2_in_2_ga₁(x₁)) = x₁
POL(append_3_in_gga₂(x₁, x₂)) = x₁ + x₂

From the DPs we obtained the following set of size-change graphs:

IF_SHUFFLE_2_IN_1_GA₁(reverse_2_out_ga₁(ZS)) -> SHUFFLE_2_IN_GA₁(ZS) (allowed arguments on rhs = {1})
The graph contains the following edges 1 >= 1
SHUFFLE_2_IN_GA₁(cons_2₁(XS)) -> IF_SHUFFLE_2_IN_1_GA₁(reverse_2_in_ga₁(XS)) (allowed arguments on rhs = {1})
The graph contains the following edges 1 > 1

We oriented the following set of usable rules.

reverse_2_in_ga₁(nil_0) -> reverse_2_out_ga₁(nil_0)
reverse_2_in_ga₁(cons_2₁(XS)) -> if_reverse_2_in_1_ga₁(reverse_2_in_ga₁(XS))
reverse_2_in_ga₁(cons_2₁(nil_0)) -> reverse_2_out_ga₁(cons_2₁(nil_0))
if_reverse_2_in_2_ga₁(append_3_out_gga₁(YS)) -> reverse_2_out_ga₁(YS)
if_reverse_2_in_1_ga₁(reverse_2_out_ga₁(ZS)) -> if_reverse_2_in_2_ga₁(append_3_in_gga₂(ZS, cons_2₁(nil_0)))
if_append_3_in_1_gga₁(append_3_out_gga₁(ZS)) -> append_3_out_gga₁(cons_2₁(ZS))
append_3_in_gga₂(nil_0, XS) -> append_3_out_gga₁(XS)
append_3_in_gga₂(cons_2₁(XS), YS) -> if_append_3_in_1_gga₁(append_3_in_gga₂(XS, YS))